fix: Don't generate the "assume T.F(ins) == C.F(ins)" statement in the function override ensures check #2504

robin-aws · 2022-07-28T00:18:41Z

As described in #2500, this assume statement (assume B.Class.TotallyNotZero(this) == A.Trait.TotallyNotZero(this); in the example) may create a contradiction if the implementation violates the trait's function specification. It is also not necessary to form the proof obligation correctly, since the trait's declaration has to have no body and therefore assuming equivalence doesn't add any additional constraint anyway.

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

# Conflicts: # Source/Dafny/Verifier/Translator.cs

robin-aws · 2022-07-28T13:55:03Z

Source/Dafny/Verifier/Translator.cs

-        argsT.Add(etran.HeapExpr);
-      }
-      // add "ordinary" parameters (including "this", if any)
-      var prefixCount = implInParams.Count - f.Formals.Count;


This seems to imply that an implementing function can have more parameters than the trait-declared version. Given that this broke zero tests, it either a) doesn't exist as a feature (anymore?), or b) has no testing coverage. My gut tells me this was implemented optimistically but never used. If no one knows the history here I can dig into it.

…e-2500

robin-aws · 2022-07-28T14:11:54Z

Source/Dafny/Verifier/Translator.cs

@@ -3475,53 +3475,29 @@ public enum StmtType { NONE, ASSERT, ASSUME };
        builder.Add(TrAssumeCmd(f.tok, etran.TrExpr(en.E)));
      }

-      //generating assume J.F(ins) == C.F(ins)


The diff here is deceptive: removing the builder.Add(TrAssumeCmd(...)) line makes half of the lines here unused, but the other half is still needed if there is a result variable declared. Consider this as a two step edit: first removing those interspersed unneeded lines, and then moving the remainder inside the if (resultVariable != null) block.

cpitclaudel · 2022-07-28T15:44:23Z

RELEASE_NOTES.md

@@ -12,6 +12,7 @@
 - feat: *Less code navigation when verifying code*: In the IDE, failing postconditions and preconditions error messages now immediately display the sub-conditions that Dafny could not prove. Both on hover and in the Problems window. (https://github.com/dafny-lang/dafny/pull/2434)
 - feat: Whitespaces and comments are kept in relevant parts of the AST (https://github.com/dafny-lang/dafny/pull/1801)
 - fix: NuGet packages no longer depend on specific patch releases of the .NET frameworks.
+- fix: Resolved unsoundness issue related to overriding functions declared in traits with `{:termination false}`. (https://github.com/dafny-lang/dafny/pull/2504) 


Wrong section of the release notes.

cpitclaudel · 2022-07-28T15:59:42Z

Test/git-issues/github-issue-2500.dfy

+      // Missing: ensures ret != 0
+    { 
+      0 
+    }


Could you give a version of this example that doesn't use {:termination false}?

cpitclaudel

Unfortunately, this fix isn't sufficient, as the fixed Dafny still accepts the following example:

module A {
  trait {:termination false} Trait {
    function method TotallyNotZero() : (ret: int)
      ensures TotallyNotZero() != 0
  }
}

module Main {
  import opened A

  class Class extends Trait {
    function method TotallyNotZero() : (ret: int) {
      0
    }
  }

  method Boom() ensures false {
    var c := new Class;
    assert c.TotallyNotZero() == 0;
    assert (c as Trait).TotallyNotZero() != 0;
  }
}

(Notice the fact that ensures now mentions TotallyNotZero)

The problem really is linked to :termination false, and specifically the fact that the postcondition of the trait function "leaks" into the override check.

cpitclaudel · 2022-07-28T19:36:35Z

After reading it, I also expected your patch to break the following case:

trait Trait {
  function method TotallyNotZero() : (ret: int)
    ensures TotallyNotZero() != 0
}

class Class extends Trait {
  function method TotallyNotZero() : (ret: int) {
    0
  }
}

Since we would get the following:

implementation {:verboseName "Class.TotallyNotZero (override check)"} OverrideCheck$$_module.Class.TotallyNotZero(this: ref) returns (ret#0: int)
{
  var Class_$_Frame: <beta>[ref,Field beta]bool;

    assert true;
    Class_$_Frame := (lambda<alpha> $o: ref, $f: Field alpha :: 
      $o != null && read($Heap, $o, alloc) ==> false);
    assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> false);
    // assert _module.Class.TotallyNotZero(this) == _module.Trait.TotallyNotZero(this);
    assume _module.Class.TotallyNotZero(this) == ret#0;
    assert _module.Trait.TotallyNotZero(this) != 0;
}

… and how would Boogie prove _module.Trait.TotallyNotZero() != 0 without knowing that _module.Class.TotallyNotZero(this) == _module.Trait.TotallyNotZero(this)? But in fact it knows that regardless of whether we comment the // line above or not:

// override axiom for _module.Trait.TotallyNotZero in class _module.Class
axiom 1 <= $FunctionContextHeight
   ==> (forall this: ref :: 
    { _module.Trait.TotallyNotZero(this), $Is(this, Tclass._module.Class()) } 
      { _module.Trait.TotallyNotZero(this), _module.Class.TotallyNotZero(this) } 
    this != null && $Is(this, Tclass._module.Class())
       ==> _module.Trait.TotallyNotZero(this) == _module.Class.TotallyNotZero(this));

(And indeed uncommenting this axiom while keeping your patch makes the valid example above fail.)

cpitclaudel · 2022-07-28T19:54:06Z

The reason I mention the override axiom is that it is "as powerful", modulo fuel issues, as the assume that this PR is removing, and in fact causes the same issue (I'm not sure it can be triggered from Dafny directly, though). Morally the issue is here:

module A {
  trait {:termination false} Trait {
    function method TotallyNotZero() : (ret: int)
      ensures ret != 0
  }
}

import opened A

class Class extends Trait {
  function method TotallyNotZero() : (ret: int)
    ensures (this as Trait).TotallyNotZero() != 0
  { 0 }
}

method Boom() ensures false {
  var c := new Class;
  assert c.TotallyNotZero() == 0;
  assert (c as Trait).TotallyNotZero() != 0;
}

The mere mention of (this as Trait).TotallyNotZero() is enough to trigger the axiom and hence restore the problem, even with the assume removed (but note that that mention also exploits :termination false, so it's cheating; adding the mention directly at the boogie level works, though).

fabiomadge · 2022-11-21T04:44:07Z

I think this PR solves the actual issue at hand. That is incorrectly performing the overrides check in a multi module setting, while correctly doing so in a single module. All the counterexamples I've seen, also rely on the lack of termination checking, which is documented.
We should add additional protection to the overrides axiom. To achieve this, I propose repurposing the $FunctionContextHeight mechanism.

robin-aws added 6 commits July 27, 2022 10:25

Test case (TTD FTW)

d75dd88

Actually runnable test

28155a8

Remove copied expect content

0e57086

Testing out just taking out the dangerous assume statement

e41e255

Fix test

5a73de9

Properly removing assume J.F(ins) == C.F(ins)

ff19d5a

# Conflicts: # Source/Dafny/Verifier/Translator.cs

robin-aws commented Jul 28, 2022

View reviewed changes

robin-aws changed the title ~~GitHub issue 2500~~ fix: Don't generate the "assume T.F(ins) == C.F(ins)" statement in the function override ensures check Jul 28, 2022

robin-aws added 2 commits July 28, 2022 07:02

Release note

9aa346a

Merge branch 'master' of github.com:dafny-lang/dafny into github-issu…

1774841

…e-2500

robin-aws marked this pull request as ready for review July 28, 2022 14:09

robin-aws requested review from cpitclaudel and RustanLeino July 28, 2022 14:09

robin-aws commented Jul 28, 2022

View reviewed changes

cpitclaudel reviewed Jul 28, 2022

View reviewed changes

cpitclaudel requested changes Jul 28, 2022

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

fix: Don't generate the "assume T.F(ins) == C.F(ins)" statement in the function override ensures check #2504

fix: Don't generate the "assume T.F(ins) == C.F(ins)" statement in the function override ensures check #2504

robin-aws commented Jul 28, 2022 •

edited

Loading

robin-aws Jul 28, 2022

robin-aws Jul 28, 2022

cpitclaudel Jul 28, 2022

cpitclaudel Jul 28, 2022

cpitclaudel left a comment •

edited

Loading

cpitclaudel commented Jul 28, 2022

cpitclaudel commented Jul 28, 2022 •

edited

Loading

fabiomadge commented Nov 21, 2022 •

edited

Loading

fix: Don't generate the "assume T.F(ins) == C.F(ins)" statement in the function override ensures check #2504

Are you sure you want to change the base?

fix: Don't generate the "assume T.F(ins) == C.F(ins)" statement in the function override ensures check #2504

Conversation

robin-aws commented Jul 28, 2022 • edited Loading

robin-aws Jul 28, 2022

Choose a reason for hiding this comment

robin-aws Jul 28, 2022

Choose a reason for hiding this comment

cpitclaudel Jul 28, 2022

Choose a reason for hiding this comment

cpitclaudel Jul 28, 2022

Choose a reason for hiding this comment

cpitclaudel left a comment • edited Loading

Choose a reason for hiding this comment

cpitclaudel commented Jul 28, 2022

cpitclaudel commented Jul 28, 2022 • edited Loading

fabiomadge commented Nov 21, 2022 • edited Loading

robin-aws commented Jul 28, 2022 •

edited

Loading

cpitclaudel left a comment •

edited

Loading

cpitclaudel commented Jul 28, 2022 •

edited

Loading

fabiomadge commented Nov 21, 2022 •

edited

Loading